<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Less-extra-indentation</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\usepackage{amsmath}
\usepackage{newunicodechar}
\newunicodechar{₁}{\ensuremath{{}_{\text{1}}}}

\pagestyle{empty}

\begin{document}

\noindent Control:
</a><a id="198" class="Markup">\begin{code}</a>
  <a id="213" href="Less-extra-indentation.html#213" class="Function">_</a> <a id="215" class="Symbol">:</a> <a id="217" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
  <a id="224" class="Symbol">_</a> <a id="226" class="Symbol">=</a> <a id="228" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="232" class="Markup">\end{code}</a><a id="242" class="Background">

\noindent No extra indentation (alignment):
</a><a id="288" class="Markup">\begin{code}[hide]</a>
  <a id="309" href="Less-extra-indentation.html#309" class="Function">_</a> <a id="311" class="Symbol">:</a> <a id="313" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
  <a id="320" class="Symbol">_</a> <a id="322" class="Symbol">=</a>
<a id="324" class="Markup">\end{code}</a><a id="334" class="Background">
</a><a id="335" class="Markup">\begin{code}</a>
    <a id="352" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="356" class="Markup">\end{code}</a><a id="366" class="Background">

\noindent No extra indentation (indentation):
</a><a id="414" class="Markup">\begin{code}[hide]</a>
  <a id="435" href="Less-extra-indentation.html#435" class="Function">_</a> <a id="437" class="Symbol">:</a> <a id="439" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
  <a id="446" class="Symbol">_</a> <a id="448" class="Symbol">=</a>
<a id="450" class="Markup">\end{code}</a><a id="460" class="Background">
</a><a id="461" class="Markup">\begin{code}</a>
     <a id="479" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="483" class="Markup">\end{code}</a><a id="493" class="Background">

\noindent No extra indentation (alignment):
</a><a id="539" class="Markup">\begin{code}[hide]</a>
  <a id="560" class="Keyword">postulate</a>
    <a id="574" href="Less-extra-indentation.html#574" class="Postulate">_</a> <a id="576" class="Symbol">:</a>
<a id="578" class="Markup">\end{code}</a><a id="588" class="Background">
</a><a id="589" class="Markup">\begin{code}</a>
      <a id="608" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="612" class="Markup">\end{code}</a><a id="622" class="Background">

\noindent No extra indentation (indentation):
</a><a id="670" class="Markup">\begin{code}[hide]</a>
  <a id="691" class="Keyword">postulate</a>
    <a id="705" href="Less-extra-indentation.html#705" class="Postulate">_</a> <a id="707" class="Symbol">:</a>
<a id="709" class="Markup">\end{code}</a><a id="719" class="Background">
</a><a id="720" class="Markup">\begin{code}</a>
       <a id="740" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="744" class="Markup">\end{code}</a><a id="754" class="Background">

\noindent No extra indentation (alignment, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
</a><a id="846" class="Markup">\begin{code}[hide]</a>
  <a id="867" href="Less-extra-indentation.html#867" class="Function">_</a> <a id="869" class="Symbol">:</a> <a id="871" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
  <a id="878" class="Symbol">_</a> <a id="880" class="Symbol">=</a>
<a id="882" class="Markup">\end{code}</a><a id="892" class="Background">
</a><a id="893" class="Markup">\begin{code}</a>
    <a id="910" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="914" class="Markup">\end{code}</a><a id="924" class="Background">
</a><a id="925" class="Markup">\begin{code}[hide]</a>
  <a id="946" href="Less-extra-indentation.html#946" class="Function">_</a> <a id="948" class="Symbol">:</a> <a id="950" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
  <a id="957" class="Symbol">_</a> <a id="959" class="Symbol">=</a>
<a id="961" class="Markup">\end{code}</a><a id="971" class="Background">
</a><a id="972" class="Markup">\begin{code}</a>
    <a id="989" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="993" class="Markup">\end{code}</a><a id="1003" class="Background">
\end{AgdaMultiCode}

\noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
</a><a id="1114" class="Markup">\begin{code}[hide]</a>
  <a id="1135" href="Less-extra-indentation.html#1135" class="Function">_</a> <a id="1137" class="Symbol">:</a> <a id="1139" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
  <a id="1146" class="Symbol">_</a> <a id="1148" class="Symbol">=</a>
<a id="1150" class="Markup">\end{code}</a><a id="1160" class="Background">
</a><a id="1161" class="Markup">\begin{code}</a>
     <a id="1179" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1183" class="Markup">\end{code}</a><a id="1193" class="Background">
</a><a id="1194" class="Markup">\begin{code}[hide]</a>
  <a id="1215" href="Less-extra-indentation.html#1215" class="Function">_</a> <a id="1217" class="Symbol">:</a> <a id="1219" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
  <a id="1226" class="Symbol">_</a> <a id="1228" class="Symbol">=</a>
<a id="1230" class="Markup">\end{code}</a><a id="1240" class="Background">
</a><a id="1241" class="Markup">\begin{code}</a>
     <a id="1259" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1263" class="Markup">\end{code}</a><a id="1273" class="Background">
\end{AgdaMultiCode}

\noindent No extra indentation (alignment, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
</a><a id="1385" class="Markup">\begin{code}[hide]</a>
  <a id="1406" class="Keyword">postulate</a>
    <a id="1420" href="Less-extra-indentation.html#1420" class="Postulate">_</a> <a id="1422" class="Symbol">:</a>
<a id="1424" class="Markup">\end{code}</a><a id="1434" class="Background">
</a><a id="1435" class="Markup">\begin{code}</a>
      <a id="1454" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1458" class="Markup">\end{code}</a><a id="1468" class="Background">
</a><a id="1469" class="Markup">\begin{code}[hide]</a>
  <a id="1490" class="Keyword">postulate</a>
    <a id="1504" href="Less-extra-indentation.html#1504" class="Postulate">_</a> <a id="1506" class="Symbol">:</a>
<a id="1508" class="Markup">\end{code}</a><a id="1518" class="Background">
</a><a id="1519" class="Markup">\begin{code}</a>
      <a id="1538" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1542" class="Markup">\end{code}</a><a id="1552" class="Background">
\end{AgdaMultiCode}

\noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
</a><a id="1663" class="Markup">\begin{code}[hide]</a>
  <a id="1684" class="Keyword">postulate</a>
    <a id="1698" href="Less-extra-indentation.html#1698" class="Postulate">_</a> <a id="1700" class="Symbol">:</a>
<a id="1702" class="Markup">\end{code}</a><a id="1712" class="Background">
</a><a id="1713" class="Markup">\begin{code}</a>
       <a id="1733" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1737" class="Markup">\end{code}</a><a id="1747" class="Background">
</a><a id="1748" class="Markup">\begin{code}[hide]</a>
  <a id="1769" class="Keyword">postulate</a>
    <a id="1783" href="Less-extra-indentation.html#1783" class="Postulate">_</a> <a id="1785" class="Symbol">:</a>
<a id="1787" class="Markup">\end{code}</a><a id="1797" class="Background">
</a><a id="1798" class="Markup">\begin{code}</a>
       <a id="1818" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1822" class="Markup">\end{code}</a><a id="1832" class="Background">
\end{AgdaMultiCode}

\noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
</a><a id="1943" class="Markup">\begin{code}[hide]</a>
  <a id="1964" class="Keyword">postulate</a>
    <a id="Aaa"></a><a id="1978" href="Less-extra-indentation.html#1978" class="Postulate">Aaa</a> <a id="1982" class="Symbol">:</a>
<a id="1984" class="Markup">\end{code}</a><a id="1994" class="Background">
</a><a id="1995" class="Markup">\begin{code}</a>
      <a id="2014" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="2018" class="Markup">\end{code}</a><a id="2028" class="Background">
</a><a id="2029" class="Markup">\begin{code}[hide]</a>
  <a id="2050" class="Keyword">postulate</a>
    <a id="Bbb"></a><a id="2064" href="Less-extra-indentation.html#2064" class="Postulate">Bbb</a> <a id="2068" class="Symbol">:</a>
<a id="2070" class="Markup">\end{code}</a><a id="2080" class="Background">
</a><a id="2081" class="Markup">\begin{code}</a>
      <a id="2100" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="2104" class="Markup">\end{code}</a><a id="2114" class="Background">
\end{AgdaMultiCode}

\end{document}
</a></pre></body></html>